Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adds several Lean backends for built-in SAIL functions (mostly arithmetic and equality) #954

Merged
merged 13 commits into from
Feb 11, 2025
Merged

Adds several Lean backends for built-in SAIL functions (mostly arithmetic and equality) #954

merged 13 commits into from
Feb 11, 2025
+140 −32

Conversation

benjaminselfridge
Copy link
Collaborator

@benjaminselfridge benjaminselfridge commented Feb 3, 2025 •
edited
Loading

Add annotations for the following SAIL builtins:

From arith.sail:

  • add_int
  • sub_int
  • negate_atom
  • negate_int
  • mult_atom
  • mul_int
  • max_int
  • min_int

From flow.sail:

  • eq_unit
  • not_bool
  • lteq_int
  • gteq_int
  • lt_int
  • gt_int

From generic_equality.sail:

  • eq_anything
  • neq_anything

@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 3, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Feb 3, 2025 •
edited
Loading

Test Results

   12 files  ±0     25 suites  ±0   0s ⏱️ ±0s
  764 tests ±0    764 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 708 runs  ±0  2 708 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit dd6414e. ± Comparison against base commit c9a9da8.

♻️ This comment has been updated with latest results.

@tobiasgrosser
Copy link
Collaborator

Can you update the description of the PR to explain what it actually adds?

@benjaminselfridge benjaminselfridge changed the title Feature/lean external arith Adds several built-in SAIL functions (mostly arithmetic and equality) Feb 3, 2025
@benjaminselfridge benjaminselfridge changed the title Adds several built-in SAIL functions (mostly arithmetic and equality) Adds several Lean backends for built-in SAIL functions (mostly arithmetic and equality) Feb 3, 2025
@javra
Copy link
Collaborator

javra commented Feb 4, 2025

Can you add the extern.expected.sail? Then the CI will go 🟢

@javra
Copy link
Collaborator

javra commented Feb 6, 2025

I think you need to overwrite the expected output once more for the CI to not complain. I always just do sail --lean-output-dir leantest/ --lean-force-output --lean test/lean/extern.sail and then mv leantest/out/Out.lean test/lean/extern.expected.lean.

@tobiasgrosser
Copy link
Collaborator

tobiasgrosser commented Feb 10, 2025 •
edited
Loading

@benjaminselfridge, we need another rebase/merge to get the conflicts resolved.

@tobiasgrosser
Copy link
Collaborator

Thank you. Did you also rebuild sail and re-generate the test cases? It seems as if this may have been missed.

@benjaminselfridge
Copy link
Collaborator Author

@!$#

I'll get used to this eventually. Just rebuilt and pushed, hopefully this is the one.

@benjaminselfridge benjaminselfridge force-pushed the feature/lean_external_arith branch from 17f594c to dd6414e Compare February 10, 2025 22:01
@benjaminselfridge
Copy link
Collaborator Author

Sorry about the churn -- I pushed to this branch again by accident! :(

@bacam bacam merged commit b689188 into rems-project:sail2 Feb 11, 2025
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@javra javra javra approved these changes

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

Assignees
No one assigned
Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@benjaminselfridge @tobiasgrosser @javra @bacam